FDL - Nuprl Lemma : sum_plus_q

Nuprl Lemma : sum_plus_q

a, b:

.
(a

b)

(

E, F:({a..b

}

).

a

i < b. E(i) + F(i) = (

a

i < b. E(i) +

a

i < b. F(i))

)

Definitions t T, t.2, t.1, CRng, <+*>, +r, x f y, |r|, x:A. B(x), a j < b. E(j)

Lemmas crng wf, qrng wf, rng sum plus